$\forall$$A$:Type, $P$:(($A$ List)$\rightarrow$Prop). safety($A$;$x$.$P$($x$)) $\in$ Prop